copilot-libraries: Add random stream generation module. Refs #766. - #788

Change Manager: Verified that:

• Solution is implemented:
  • The code proposed compiles and passes all tests. Details:
    Build log: https://github.com/Copilot-Language/copilot/runs/125637752921
  • The solution proposed produces the expected result. Details:
    The following Dockerfile checks that the numbers produced for 32-bits do not have an extreme frequency of zeroes or ones in binary representation, and there are not too many consecutive values that are the same, after which it prints the message "Success":

    --- Dockerfile-verify-766
    FROM ubuntu:jammy
    
    WORKDIR /root
    SHELL ["/bin/bash", "-c"]
    
    ENV DEBIAN_FRONTEND=noninteractive
    RUN apt-get update
    
    RUN apt-get install --yes \
          bc \
          curl \
          g++ \
          gcc \
          git \
          libgmp3-dev  \
          libz-dev \
          make \
          pkg-config \
          z3
    
    RUN mkdir -p $HOME/.ghcup/bin
    RUN curl https://downloads.haskell.org/~ghcup/0.1.40.0/x86_64-linux-ghcup-0.1.40.0 -o $HOME/.ghcup/bin/ghcup
    RUN chmod a+x $HOME/.ghcup/bin/ghcup
    ENV PATH=$PATH:/root/.ghcup/bin/
    ENV PATH=$PATH:/root/.cabal/bin/
    
    RUN ghcup install ghc 9.10.1
    RUN ghcup install cabal 3.2
    RUN ghcup set ghc 9.10.1
    RUN cabal user-config init
    RUN sed -i -e "s;-- \(secure.\) True;\1 False;g" /root/.cabal/config
    RUN cabal update
    
    ARG GIT_COMMIT=HEAD
    ARG NAME=copilot
    ARG REPO=https://github.com/copilot-language/copilot
    
    RUN git clone ${REPO} ${NAME}
    RUN cd ${NAME} && git checkout ${GIT_COMMIT}
    
    WORKDIR ${NAME}
    
    RUN cabal v1-sandbox init
    RUN cabal v1-install alex happy
    
    RUN cabal v1-install \
          copilot/ \
          copilot-c99/ \
          copilot-core/ \
          copilot-interpreter/ \
          copilot-language/ \
          copilot-libraries/ \
          copilot-prettyprinter/ \
          copilot-theorem/
    
    ADD TestRandom.hs /tmp/
    RUN cabal v1-exec -- runhaskell /tmp/TestRandom.hs
    
    --- TestRandom.hs
    {-# LANGUAGE DataKinds #-}
    
    module Main where
    
    import           Control.Monad          ( forM_, when )
    import           Copilot.Interpret.Eval ( ShowType (Haskell), eval,
                                              interpTriggers )
    import           Copilot.Language       hiding ( drop, (&&), (++), (/=), (==),
                                              (>) )
    import           Copilot.Language.Reify ( reify )
    import qualified Copilot.Library.Random as R
    import           Data.Bits              ( testBit )
    import           Data.Maybe             ( catMaybes, mapMaybe )
    import           System.Exit            ( exitSuccess )
    import           System.IO              ( hPutStrLn, stderr )
    import           Text.Read              ( readMaybe )
    
    main :: IO ()
    main = do
      randomValues32 <- fmap (concat . catMaybes)
                        <$> lookup "random32"
                        <$> interpTriggers
                        <$> eval Haskell samples
                        <$> reify spec32
    
      ifMaybe randomValues32 (error "Random values not obtained") $ \randomValues32' -> do
    
        when (length randomValues32' /= samples) $
          error "random32 values missing"
    
        let values32 = parseValues randomValues32' :: [Word32]
    
        results <- sequence
          [ checkBits "randomW32" 32 values32
          , checkDuplicates "randomW32" values32
          ]
    
        if and results
          then do
            putStrLn "Success"
          else do
            error "Statistical tests failed"
    
    samples :: Integral a => a
    samples = 1000
    
    spec32 :: Spec
    spec32 =
      trigger "random32" (constant True) [arg (R.randomW32 1234567 7654321)]
    
    -- | Check that the frequence of zeroes or ones in binary reprentations are not
    -- disproportionally swayed one way or another.
    checkBits :: (Bits a, Integral a) => String -> Int -> [a] -> IO Bool
    checkBits name width xs = do
      -- A six-sigma threshold makes accidental failures very unlikely.
      let n           = length xs
          expected    = fromIntegral n / 2 :: Double
          sigma       = sqrt (fromIntegral n / 4 :: Double)
          frequencies = bitCounts width xs
          runs        = transitions width xs
          runExpected = fromIntegral (n - 1) / 2 :: Double
          runSigma    = sqrt (fromIntegral (n - 1) / 4 :: Double)
    
          badFrequency =
            [ (i, count)
            | (i, count) <- zip [0..] frequencies
            , abs (fromIntegral count - expected) > 6 * sigma
            ]
    
          badRuns =
            [ (i, count)
            | (i, count) <- zip [0..] runs
            , abs (fromIntegral count - runExpected) > 6 * runSigma
            ]
    
      putStrLn $ name ++ ": " ++ show n ++ " samples"
    
      forM_ badFrequency $ \(i, count) ->
        hPutStrLn stderr $ "Bit " ++ show i ++ " frequency = " ++ show count
    
      forM_ badRuns $ \(i, count) ->
        hPutStrLn stderr $ "Bit " ++ show i ++ " transitions = " ++ show count
    
      return (null badFrequency && null badRuns)
    
    -- | Count occurrences of set bits.
    bitCounts :: (Bits a, Integral a) => Int -> [a] -> [Int]
    bitCounts width xs =
      [ length (filter (`testBit` bit) xs) | bit <- [0 .. width - 1] ]
    
    -- | Count transitions between consecutive bits.
    transitions :: (Bits a, Integral a) => Int -> [a] -> [Int]
    transitions width xs =
      [ length
          [ () | (a, b) <- zip xs (drop 1 xs), testBit a bit /= testBit b bit ]
      | bit <- [0 .. width - 1]
      ]
    
    -- | Check if a list contains duplicates.
    checkDuplicates :: (Eq a, Show a) => String -> [a] -> IO Bool
    checkDuplicates name xs = do
      let duplicates = length [ () | (a, b) <- zip xs (drop 1 xs), a == b ]
    
      putStrLn $ name ++ ": " ++ show duplicates ++ " consecutive duplicate values"
    
      if duplicates > 3
        then do
          hPutStrLn stderr "Too many consecutive duplicates"
          return False
        else return True
    
    -- * Auxiliary functions
    
    -- | Flipped version of maybe that renders more convenient notation.
    ifMaybe :: Maybe a -> b -> (a -> b) -> b
    ifMaybe m d f = maybe d f m
    
    -- | Extract numeric values from the interpreter output.
    parseValues :: Read a => [String] -> [a]
    parseValues = mapMaybe (readMaybe . unwords . words)
    

    Command (substitute variables based on new path after merge):

    $ docker build --build-arg "REPO=https://github.com/jamestoddgloyd/copilot" --build-arg "NAME=copilot" --build-arg "GIT_COMMIT=39548759d483719d4554bf8cd2e21adf5a8b21aa" -t copilot-verify-766 -f Dockerfile-verify-766 .
    

• Implementation is documented. Details:
  The module includes documentation.
• Change history is clear.
• Commit messages are clear.
• Changelogs are updated.
• Examples are updated. Details:
  No updates needed; the change introduces a module but does not affect existing examples.
• Author is internal or has provided signed CLA.
• Required version bumps are evaluated. Details:
  Bump not needed; change extends API but does not alter existing definitions.